(set-logic QF_BV)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const bv_1-0 (_ BitVec 1))
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const bv_3-0 (_ BitVec 3))
(assert (or v22))
(assert (or v25 v5 v0 v5))
(assert (or v22 v1 v22 v0 v22 (xor v13 v1 v12 v4 v5)))
(assert (or v22))
(assert (or v25 v25 (xor v13 v1 v12 v4 v5) v22 v5 v5 v22 v25 v1 v5))
(assert (or v1 v0))
(assert (or v25 v0))
(assert (or v22 v5))
(assert (or v0 v22 v0))
(assert (or v5))
(assert (or v25 v25 v0 v5))
(assert (or v0 v1 v0 (xor v13 v1 v12 v4 v5) v0))
(assert (or v22))
(assert (or (xor v13 v1 v12 v4 v5) v25 v5 v0 (xor v13 v1 v12 v4 v5)))
(assert (or (xor v13 v1 v12 v4 v5) (xor v13 v1 v12 v4 v5) v22))
(assert (or v22 v1 v22))
(minimize bv_1-0)
(minimize bv_3-0)
(check-sat)
(exit)
